\begin{tabbing}
(\=Unfold `can{-}apply` ( 0)$\cdot$) \+
\\[0ex]CollapseTHEN (((InductionOnNat) 
\\[0ex]CollapseTHEN (Auto$\cdot$)$\cdot$) 
\\[0ex]
\\[0ex]CollapseTHEN ((CaseNat 0 `m') 
\\[0ex]CollapseTHEN (((Try ((RepUR ``p{-}fun{-}exp p{-}compose p{-}id
\-\\[0ex]`\=` ( 0)$\cdot$) \+
\\[0ex]CollapseTHEN (Trivial)$\cdot$))$\cdot$) 
\\[0ex]CollapseTHEN ((Subst' $m$ $\sim$ (($m$ {-} 1)+1) ( 0)$\cdot$) 
\\[0ex]
\\[0ex]CollapseTHEN (((Try ((Complete (Auto'))$\cdot$))$\cdot$) 
\\[0ex]CollapseTHEN ((RWO "p{-}fun{-}exp{-}add" 0) 
\\[0ex]
\\[0ex]CollapseTHEN ((Auto$\cdot$) 
\\[0ex]CollapseTHEN ((MoveToConcl ({-}4)) 
\\[0ex]CollapseTHEN ((Subst' $n$\=\+
\\[0ex]$\sim$
\\[0ex](($n$ {-} 1)
\\[0ex]+1) ( 0)
\-\-\\[0ex]$\cdot$\=) \+
\\[0ex]CollapseTHEN (((Try ((Complete (Auto'))$\cdot$))$\cdot$) 
\\[0ex]CollapseTHEN ((RWO "p{-}fun{-}exp{-}add" 0)
\\[0ex]
\\[0ex]CollapseTHENA (Auto$\cdot$)$\cdot$)$\cdot$)$\cdot$)$\cdot$)$\cdot$)$\cdot$)$\cdot$)$\cdot$)$\cdot$)$\cdot$)$\cdot$)$\cdot$
\-
\end{tabbing}